|
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its existence, according to constructivism. This viewpoint involves a verificational interpretation of the existence quantifier, which is at odds with its classical interpretation. There are many forms of constructivism.〔Troelstra 1977a:974〕 These include the program of intuitionism founded by Brouwer, the finitism of Hilbert and Bernays, the constructive recursive mathematics of Shanin and Markov, and Bishop's program of constructive analysis. Constructivism also includes the study of constructive set theories such as IZF and the study of topos theory. Constructivism is often identified with intuitionism, although intuitionism is only one constructivist program. Intuitionism maintains that the foundations of mathematics lie in the individual mathematician's intuition, thereby making mathematics into an intrinsically subjective activity.〔Troelstra 1977b:1〕 Other forms of constructivism are not based on this viewpoint of intuition, and are compatible with an objective viewpoint on mathematics. == Constructive mathematics == Much constructive mathematics uses intuitionistic logic, which is essentially classical logic without the law of the excluded middle. This law states that, for any proposition, either that proposition is true or its negation is. This is not to say that the law of the excluded middle is denied entirely; special cases of the law will be provable. It is just that the general law is not assumed as an axiom. The law of non-contradiction (which states that contradictory statements cannot both at the same time be true) is still valid. For instance, in Heyting arithmetic, one can prove that for any proposition ''p'' that ''does not contain quantifiers'', is a theorem (where ''x'', ''y'', ''z'' ... are the free variables in the proposition ''p''). In this sense, propositions restricted to the finite are still regarded as being either true or false, as they are in classical mathematics, but this bivalence does not extend to propositions that refer to infinite collections. In fact, L.E.J. Brouwer, founder of the intuitionist school, viewed the law of the excluded middle as abstracted from finite experience, and then applied to the infinite without justification. For instance, Goldbach's conjecture is the assertion that every even number (greater than 2) is the sum of two prime numbers. It is possible to test for any particular even number whether or not it is the sum of two primes (for instance by exhaustive search), so any one of them is either the sum of two primes or it is not. And so far, every one thus tested has in fact been the sum of two primes. But there is no known proof that all of them are so, nor any known proof that not all of them are so. Thus to Brouwer, we are not justified in asserting "either Goldbach's conjecture is true, or it is not." And while the conjecture may one day be solved, the argument applies to similar unsolved problems; to Brouwer, the law of the excluded middle was tantamount to assuming that ''every'' mathematical problem has a solution. With the omission of the law of the excluded middle as an axiom, the remaining logical system has an existence property that classical logic does not: whenever is proven constructively, then in fact is proven constructively for (at least) one particular , often called a witness. Thus the proof of the existence of a mathematical object is tied to the possibility of its construction. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Constructivism (mathematics)」の詳細全文を読む スポンサード リンク
|